Nuprl Lemma : es-shift_wf2
11,40
postcript
pdf
es
:ES,
i
:Id,
t
:
,
s
:es_state(
es
;
i
).
s
+
t
es_state(
es
;
i
)
latex
Definitions
ES
,
t
T
,
Id
,
,
x
:
A
.
B
(
x
)
,
es-T(
es
)
,
f
(
a
)
,
EState(
T
)
,
s
+
r
,
es_vartype(
es
;
i
;
x
)
,
es_state(
es
;
i
)
Lemmas
es-shift
wf
,
EState
wf
,
es-T
wf
,
rationals
wf
,
Id
wf
,
event
system
wf
origin
es:ES, i:Id, t:
, s:es_state(es;i). s+t 
es_state(es;i) es:ES, i:Id, t:, s:es_state(es;i). s+t es_state(es;i) Tx:A. B(x)